\begin{tabbing}
$\forall$${\it the\_w}$:World, $e$:E.
\\[0ex]FairFifo
\\[0ex]$\Rightarrow$ isrcv(kind($e$))
\\[0ex]$\Rightarrow$ (\=$\exists$$t$:$\mathbb{N}$$_{\mbox{\scriptsize $<$time($e$)}}$.\+
\\[0ex]match(lnk(kind($e$));$t$;time($e$))
\\[0ex]\& \=0$\leq\parallel$rcvs(lnk(kind($e$));time($e$))$\parallel-\parallel$snds(lnk(kind($e$));$t$)$\parallel$\+
\\[0ex]\& \=$\parallel$rcvs(lnk(kind($e$));time($e$))$\parallel$\+
\\[0ex]$-\parallel$snds(lnk(kind($e$));$t$)$\parallel<\parallel$onlnk(lnk(kind($e$));m(source(lnk(kind($e$)));$t$))$\parallel$
\-\\[0ex]\& \=onlnk(lnk(kind($e$));m(source(lnk(kind($e$)));$t$))\+
\\[0ex][$\parallel$rcvs(lnk(kind($e$));time($e$))$\parallel-\parallel$snds(lnk(kind($e$));$t$)$\parallel$]
\\[0ex]$=$
\\[0ex]msg(a(loc($e$);time($e$)))
\\[0ex]$\in$ Msg)
\-\-\-
\end{tabbing}